COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	\input basic 
C00010 00003
C00011 ENDMK
C⊗;
\input basic 

\ctrline{MODAL KNOWLEDGE AXIOMS AND THEIR TRANSLATION TO FIRST ORDER LOGIC}


	Around 1960 I developed a modal system of
axioms for knowledge.  This system was adequate to formalize the problem
of the three wise men with spots on their foreheads in the usual form
in which it is stated that the first two wise men don't know the
colors of their spots.  However, I
put off publishing, because I couldn't
the modal formalism was inadequate to express the reasoning involved in
proving that the first two wise ment don't know the colors of their spots.

	When I presented it in my seminar in Kyoto in 1975,
it was much further developed by Sato, Hayashi and Igarashi who
developed several improvements and extensions.  In particular, Sato's
thesis (1977) gave it a Kripke style semantics, which can be used to prove
non-knowledge in some cases.
It is now worth describing in
connection with the relation between modal systems of axioms and
their translation into ordinary first order logic.

	$S$ knows $p$, where $S$ is a person and $p$ is a sentence,
is denoted by $S\ast p$.  There is a special person called ``any fool''
denoted by $0$.  The sentences are built up from propositional constants
using the logical operators and the knowledge operators, $S1\ast ,$ $S2\ast ,$ etc.
where $S1,$ $S2,$ etc. are constants denoting persons.

	We sometimes use the abbreviation $S\$p$ for $S\ast p ∨ S\ast ¬p$
and read it ``$S$ knows whether $p$''.

	Three systems called KTM, KT4, and KT5 are defined.
Each of them has all instances of the following schemata as axioms
and modus ponens as the sole rule of inference.

K:	$0\ast π$ (where $π$ is any instance of a propositional calculus tautology
including those formed using $S\ast $); Any fool knows tautologies.

K0:	$S\ast p ⊃ p$; What someone knows is true.

K1:	$0\ast (S\ast p ⊃ p)$; Any fool knows the above.

K2:	$0\ast (0\ast p ⊃ 0\ast S\ast p)$; Any fool knows that what any fool knows, any fool
knows everyone knows.

K3:	$0\ast (S\ast p ∧ S\ast (p ⊃ q) ⊃ S\ast q)$; Any fool knows that anyone
 can do modus ponens.

	KT4 has the additional schema

K4:	$0\ast (S\ast p ⊃ S\ast S\ast p)$; Any fool knows that if someone knows something, he
knows he knows it.

	KT5 has the additional schema

K5:	$0\ast (¬S\ast p ⊃ S\ast (¬S\ast p))$; Any fool knows that if someone doesn't know
something, he knows he doesn't know it.  This can also be written
$0\ast S\$ S\ast p$.

	Notice that there is no rule resembling the {\it necessitation} rule
of modal logic.  Its place is taken by the properties of $0\ast $.
Necessitation is unwanted, because we require a system that can deal with
contingent facts as well as necessary ones.

	The following facts about these systems have been proved by
various people:

	1. If $0$ is the only individual, then the schemata K, K0, $\ldots $,
K3 give a system equivalent to the modal system S5, where $0\ast p$ is
read ``$p$ is necessary''.

	2. The theorems of KTM, KT4, and KT5 involving a single person
letter (say $S1$) that is not $0$ correspond to the theorems of the modal
systems M, S4, and S5 respectively.

	3. If K5 is present, then K4 can be omitted.  This corresponds
to the fact that S4 is included in S5.

	4. We can axiomatize the puzzle of the three wise men in the
following way.


Sample theorem: $S1\ast S2\ast p ⊃ S1 \ast p.$

Proof:

1. $0\ast [0\ast (S2\ast p ⊃ p) ⊃ 0 \ast S1\ast (S2\ast p ⊃ p)]$, K2

2. $0\ast (S2\ast p ⊃ p) ⊃ 0\ast S1\ast (S2\ast p ⊃ p)$, 1, K0 and m.p.

3. $0\ast (S2\ast p ⊃ p)$, K1

4. $0\ast S1\ast (S2\ast p ⊃ p)$, 2,3 and m.p.

5. $S1\ast (S2\ast p ⊃ p)$, 4, K0 and m.p.

6. $0\ast [S1\ast S2\ast p ∧ S1\ast (S2\ast p ⊃ p) ⊃ S1\ast p]$, K3

7. $S1\ast S2\ast p ∧ S1\ast (S2\ast p ⊃ p) ⊃ S1\ast p$, 6, K0 and m.p.

8. $S1\ast S2\ast p ⊃ S1\ast p$, tautologous from 5 and 7.


	The problem of the three wisemen can be expressed as follows:

Let $S1$, $S2$ and $S3$ be the three wisemen, and let $p1$, $p2$ and $p3$
be the propositions that their respective spots are white.  The situation
is described by the sentences

1. $0\ast (p1∨p2∨p3$).  They jointly know at least one spot is white.

2. $p1 ∧ p2 ∧ p3$.  The spots are all white.

3. $0\ast (S1\$p2 ∧ S1\$p3 ∧ S2\$p1 ∧ S2\$p3 ∧ S3\$p1 ∧ S3\$p2)$.  Each can
see the spots of the foreheads of the others.

4. $S3\ast S2\$ S1\ast p1$.  $S3$ knows that $S2$ knows whether $S1$ knows $p1$.

5. $S3\$ S2\ast p2$.  $S3$ knows whether $S2$ knows that $p2$.

6. $¬S1\ast p1$.  $S1$ does not know $p1$.

7. $¬S2\ast p2$.  $S2$ does not know $p2$.

	The problem is to prove $S3\ast p3$, i.e. that the third wiseman
knows the color of his spot.

\vfill\end